(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)

Require Import Matrix.Mat.Mat_make.
Require Export Matrix.Mat.Matrix_Module.
Require Import ZArith.
Open Scope Z_scope.

Section Lemma_needed.

Lemma Zplus_assoc: forall a b c:Z,
  a + b + c = a + (b + c).
Proof. intros. ring. Qed.

Lemma Zplus_assoc2: forall a b c d:Z,
  (a + b) + (c + d) = (a + c) + (b + d).
Proof. intros. ring. Qed.

Lemma Zminus_assoc: forall a b c:Z,
  a - b - c = a - (b + c).
Proof. intros. ring. Qed.

Lemma Zminus_assoc2 :forall a b c d:Z,
  (a + b) - (c + d) = (a - c) + (b - d).
Proof. intros. ring. Qed.

Lemma Zminus_opp : forall a b :Z,
  a - b = - (b - a).
Proof. intros. ring. Qed.

Lemma Zminus_self: forall a :Z,
  a - a = 0.
Proof. intros. ring. Qed.

Lemma Zmul_assoc: forall a b c:Z,
  a * b * c = a * (b * c).
Proof. intros. ring. Qed.

End Lemma_needed.
Module ZM.

Definition A := Z.
Definition One := 1.
Definition Zero := 0.

Definition opp := Z.opp.
Definition add := Z.add.
Definition sub := Z.sub.
Definition mul := Z.mul.

Definition add_comm := Zplus_comm.
Definition add_assoc := Zplus_assoc.
Definition add_assoc2:= Zplus_assoc2.
Definition add_zero_l:= Zplus_0_l.
Definition add_zero_r := Zplus_0_r.

Definition sub_assoc := Zminus_assoc.
Definition sub_assoc2:= Zminus_assoc2.
Definition sub_opp := Zminus_opp.
Definition sub_zero_l := Z.sub_0_l.
Definition sub_zero_r := Z.sub_0_r.
Definition sub_self := Zminus_self.

Definition mul_add_distr_l:= Z.mul_add_distr_r.
Definition mul_add_distr_r := Z.mul_add_distr_l.
Definition mul_sub_distr_l := Z.mul_sub_distr_r.
Definition mul_sub_distr_r := Z.mul_sub_distr_l.
Definition mul_assoc := Zmul_assoc.
Definition mul_zero_l := Z.mul_0_l.
Definition mul_zero_r := Z.mul_0_r.
Definition mul_one_l:= Z.mul_1_l.
Definition mul_one_r:= Z.mul_1_r.
Definition mul_comm := Z.mul_comm.

End ZM.

Module ZMatrix := Matrix(ZM).

Definition ZMtrans := @ZMatrix.Mtrans.
Arguments ZMtrans {m} {n}.

Definition ZMadd := @ZMatrix.Madd.
Arguments ZMadd {m} {n}.

Definition ZMsub := @ZMatrix.Msub.
Arguments ZMsub {m} {n}.

Definition ZMopp := @ZMatrix.Mopp.
Arguments ZMopp {m} {n}.

Definition ZMmul := @ZMatrix.Mmul.
Arguments ZMmul {m} {n} {p}.

Definition ZMmulc_l := @ZMatrix.Mmulc_l.
Arguments ZMmulc_l {m} {n}.

Definition ZMmulc_r := @ZMatrix.Mmulc_r.
Arguments ZMmulc_r {m} {n}.

Definition ZMO := @ZMatrix.MO.

Definition ZMI := @ZMatrix.MI.

Notation "m1 ZM+ m2" := (ZMadd m1 m2) (at level 65).

Notation "m1 ZM- m2" := (ZMsub m1 m2) (at level 65).

Notation " ZM- m" := (ZMopp m) (at level 65).

Notation "m1 ZM* m2" := (ZMmul m1 m2) (at level 60).

Notation "c ZC* m" := (ZMmulc_l c m) (at level 60).

Notation "m *ZC c" := (ZMmulc_r m c) (at level 60).

(*Definition ZMeq_visit := @ZMatrix.Meq_visit.
Arguments ZMeq_visit {m} {n}. *)

Definition ZMadd_comm := @ZMatrix.Madd_comm.
Arguments ZMadd_comm {m} {n}.

Definition ZMadd_assoc := @ZMatrix.Madd_assoc.
Arguments ZMadd_assoc {m} {n}.

Definition ZMadd_zero_l := @ZMatrix.Madd_zero_l.
Arguments ZMadd_zero_l {m} {n}.

Definition ZMadd_zero_r := @ZMatrix.Madd_zero_r.
Arguments ZMadd_zero_r {m} {n}.

Definition ZMsub_comm := @ZMatrix.Msub_comm.
Arguments ZMsub_comm {m} {n}.

Definition ZMsub_assoc := @ZMatrix.Msub_assoc.
Arguments ZMsub_assoc {m} {n}.

Definition ZMsub_O_l := @ZMatrix.Msub_O_l.
Arguments ZMsub_O_l {m} {n}.

Definition ZMsub_O_r := @ZMatrix.Msub_O_r.
Arguments ZMsub_O_r {m} {n}.

Definition ZMsub_self := @ZMatrix.Msub_self.
Arguments ZMsub_self {m} {n}.

Definition ZMmul_distr := @ZMatrix.Mmul_add_distr_l.
Arguments ZMmul_distr {m} {n}.

Definition ZMmul_assoc:= @ZMatrix.Mmul_assoc.
Arguments ZMmul_assoc {m} {n} {p} {k}.

Definition ZMmul_zero_l:=@ZMatrix.Mmul_zero_l.
Arguments ZMmul_zero_l {m} {n}.

Definition ZMmul_zero_r:=@ZMatrix.Mmul_zero_r.
Arguments ZMmul_zero_r {m}{n}.

Definition ZMmul_mul_unit_l := @ZMatrix.Mmul_unit_l.
Arguments ZMmul_mul_unit_l {m} {n}.

Definition ZMmul_mul_unit_r := @ZMatrix.Mmul_unit_r.
Arguments ZMmul_mul_unit_r {m} {n}.

Definition ZMmulc_comm := @ZMatrix.Mmulc_comm.
Arguments ZMmulc_comm {m} {n}.

Definition ZMmulc_distr_l :=@ZMatrix.Mmulc_distr_l.
Arguments ZMmulc_distr_l {m} {n}.

Definition ZMmulc_0_l:=@ZMatrix.Mmulc_0_l.
Arguments ZMmulc_0_l {m} {n}.

Definition ZMtteq := @ZMatrix.Mtteq.
Arguments ZMtteq {m} {n}.

Definition ZMcteq := @ZMatrix.Mcteq.
Arguments ZMcteq {m} {n}.

Definition ZMteq_add := @ZMatrix.Mteq_add.
Arguments ZMteq_add {m} {n}.

Definition ZMteq_sub := @ZMatrix.Mteq_sub.
Arguments ZMteq_sub {m} {n}.

Definition ZMteq_mul := @ZMatrix.Mteq_mul.
Arguments ZMteq_mul {m} {n}.

Definition ZMtrans_MI:= @ZMatrix.Mtrans_MI.
Arguments ZMtrans_MI {n}.

Require Export Setoid.
Require Export Relation_Definitions.
Set Implicit Arguments.

Add Parametric Relation {m n:nat} : (Mat Z m n) (@M_eq Z m n) 
  reflexivity proved by (@Meq_ref Z m n)
  symmetry proved by (@Meq_sym Z m n)
  transitivity proved by (@Meq_trans Z m n)
  as ZMeq_rel.


Lemma Zmat_add_compat : 
  forall m n, 
     forall x x' : (Mat Z m n ), @M_eq Z m n x x' ->
     forall y y' : (Mat Z m n ), @M_eq Z m n y y'->
        @M_eq Z m n (ZMadd x y) (ZMadd x' y').
Proof.
  intros.
  unfold ZMadd,ZMatrix.Madd. rewrite H,H0.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@ZMadd m n)
  with signature (@M_eq Z m n) ==> (@M_eq Z m n) ==> (@M_eq Z m n) 
  as Zmat_add_mor.
Proof.
exact (@Zmat_add_compat m n).
Qed.

Lemma Zmat_sub_compat : 
  forall m n, 
     forall x x' : (Mat Z m n ), @M_eq Z m n x x' ->
     forall y y' : (Mat Z m n ), @M_eq Z m n y y'->
        @M_eq Z m n (ZMsub x y) (ZMsub x' y').
Proof.
  intros.
  unfold ZMsub,ZMatrix.Msub. rewrite H,H0.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@ZMsub m n)
  with signature (@M_eq Z m n) ==> (@M_eq Z m n) ==> (@M_eq Z m n) 
  as Zmat_sub_mor.
Proof.
exact (@Zmat_sub_compat m n).
Qed.

Lemma Zmat_opp_compat : 
  forall m n, 
     forall x x' : (Mat Z m n ), @M_eq Z m n x x' ->
        @M_eq Z m n (ZMopp x ) (ZMopp x' ).
Proof.
  intros.
  unfold ZMopp,ZMatrix.Mopp. rewrite H.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@ZMopp m n)
  with signature (@M_eq Z m n) ==> (@M_eq Z m n)
  as Zmat_opp_mor.
Proof.
exact (@Zmat_opp_compat m n).
Qed.

Lemma Zmat_trans_compat : 
  forall m n, 
     forall x x' : (Mat Z m n ), @M_eq Z m n x x' ->
        @M_eq Z n m (ZMtrans x ) (ZMtrans x' ).
Proof.
  intros.
  unfold ZMtrans,ZMatrix.Mtrans. rewrite H.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@ZMtrans m n)
  with signature (@M_eq Z m n) ==> (@M_eq Z n m)
  as Zmat_trans_mor.
Proof.
exact (@Zmat_trans_compat m n).
Qed.

Lemma Zmat_mul_compat : 
  forall m n p, 
     forall x x' : (Mat Z m n ), @M_eq Z m n x x' ->
     forall y y' : (Mat Z n p ), @M_eq Z n p y y'->
        @M_eq Z m p (ZMmul x y) (ZMmul x' y').
Proof.
  intros.
  unfold ZMmul,ZMatrix.Mmul. rewrite H,H0.
  reflexivity.
Qed.

Add Parametric Morphism {m n p :nat}:(@ZMmul m n p)
  with signature (@M_eq Z m n) ==> (@M_eq Z n p) ==> (@M_eq Z m p) 
  as Zmat_mul_mor.
Proof.
exact (@Zmat_mul_compat m n p).
Qed.





